Definition Update(st: State)(id: Id)(val: Val) : State :=
  fun (id': Id) => if (equal_id id id') then Some val else st id'.